package com.mikelouis.test.scala.proginscala.scalacheck

/**
 * 前面我们描述了如何使用ScalaCheck针对程序的孤立部分、代码单元(通常是方法)声明属性, 以及如何以自动化的方式对这些属性测试。
 * 不过有时我们不仅仅需要声明单个方法独立运行的行为，同时也需要对方法集合作为一个整体、比如作为一个大系统的接口、的行为进行声明。
 * 我们需要对在系统存续时间内方法、或者说命令影响系统的状态的方式进行声明
 *
 * Created by yuazhu on 4/21/2015.
 */
object StatefulTesting {

  // 一个可能的例子是声明ATM的工作流。我们想声明这样的需求, 在任何钱被取出之前用户必需输入正确的PIN 码,又如输入错误密码三次会导致机器没收信用卡
  // 使用ScalaCheck的属性组合子来形式化这些命令序列会有些困难。作为替代、有一个小的库org.scalacheck.Commands可以对命令建模并且对它们声明条件,
  // 然后这些声明可以像普通的ScalaCheck属性一样，可以由模块org.scalacheck.Test测试
  class Counter {
    private var n = 0

    def inc = n += 1

    def dec = n -= 1

    def get = n

    def reset = n = 0
  }

//  import org.scalacheck.commands.Commands
//
//  object CounterSpecification extends Commands {
//
//    // 这是被测试的系统。所有的命令针对这个实例运行
//    // This is our system under test. All commands run against this instance.
//    val counter = new Counter
//
//    // 这是封装了抽象状态的状态类型。抽象状态应该对实际状态、即被测试的系统中我们需要的所有特性建模。
//    // 我们应该省略掉为声明前置条件和后置条件所不需要的细节。这个状态类型被称为State并且不可变。
//    // This is our state type that encodes the abstract state. The abstract state
//    // should model all the features we need from the real state, the system
//    // under test. We should leave out all details that aren't needed for
//    // specifying our pre- and postconditions. The state type must be called
//    // State and be immutable.
//    case class State(n: Int)
//
//    // 初始状态应该重置系统到一个良好定义的初始的状态, 并返回状态的抽象版本。
//    // initialState should reset the system under test to a well defined
//    // initial state, and return the abstract version of that state.
//    def initialState() = {
//      counter.reset
//      State(counter.get)
//    }
//
//    // 我们定义命令为特质类 Command 或者 SetCommand的子类。每个命令必须拥有一个run方法、一个返回新抽象状态的方法,
//    // 这是由于它需要查看所执行的命令。命令也能够定义前置条件、声明如果命令被允许执行时当前抽象状态的样子。最后
//    // 也可以定义后置条件、验证被测试的系统在命令执行后处于一个正确的状态。
//    // We define our commands as subtypes of the traits Command or SetCommand.
//    // Each command must have a run method and a method that returns the new
//    // abstract state, as it should look after the command has been run.
//    // A command can also define a precondition that states how the current
//    // abstract state must look if the command should be allowed to run.
//    // Finally, we can also define a postcondition which verifies that the
//    // system under test is in a correct state after the command exectution.
//
//    case object Inc extends Command {
//      def run(s: State) = counter.inc
//
//      def nextState(s: State) = State(s.n + 1)
//
//      // 如果想定义前置条件, 需要添加一个接受当前抽象状态作为参数并返回boolean值的函数,
//      // 这个boolean值表示前置条件是否满足。在本例中, 我们不需要前置条件，所以我们只是让这个函数返回真。
//      // 显然, 我们原本可以省略添加这个前置条件的。
//      // if we want to define a precondition, we add a function that
//      // takes the current abstract state as parameter and returns a boolean
//      // that says if the precondition is fulfilled or not. In this case, we
//      // have no precondition so we just let the function return true. Obviously,
//      // we could have skipped adding the precondition at all.
//      preConditions += (s => true)
//
//    }
//
//    case object Dec extends Command {
//      def run(s: State) = counter.dec
//
//      def nextState(s: State) = State(s.n - 1)
//    }
//
//    case object Get extends Command {
//      def run(s: State) = counter.get
//
//      def nextState(s: State) = s
//
//      // 在定义后置条件时, 需要添加一个函数, 这个函数接受三个参数,s0, s1和r。s0是命令运行前的抽象状态。
//      // s1是命令执行后的状态, r是命令运行的结果。这个后置条件函数返回一个表示条件是否为真的boolean值(或者一个Prop的实例)。
//      // when we define a postcondition, we add a function that
//      // takes three parameters, s0, s1 and r. s0 is the abstract state before
//      // the command was run, s1 is the state after the command was run
//      // and r is the result from the command's run method. The
//      // postcondition function should return a Boolean (or
//      // a Prop instance) that says if the condition holds or not.
//      postConditions += {
//        case (s0, s1, r: Int) => r == s0.n
//        case _ => false
//      }
//    }
//
//    // 这个是命令生成器。给定一个抽象状态，这个生成器应该返回一个在这个状态下允许被执行的命令。
//    // 请注意，如果命令需要任何前置条件，那么仍然要定义这些前置条件。
//    // 生成器仅仅返回一个在给定状态适合的命令的提示, 前置条件仍然会在命令执行前被检查。
//    // 有时可能需要根据状态或者基于状态的其它运算来调整命令生成器的生成分布。
//    // This is our command generator. Given an abstract state, the generator
//    // should return a command that is allowed to run in that state. Note that
//    // it is still neccessary to define preconditions on the commands if there
//    // are any. The generator is just giving a hint of which commands that are
//    // suitable for a given state, the preconditions will still be checked before
//    // a command runs. Sometimes you maybe want to adjust the distribution of
//    // your command generator according to the state, or do other calculations
//    // based on the state.
//    def genCommand(s: State): Gen[Command] = Gen.oneOf(Inc, Dec, Get)
//
//  }

}
